crng\{i:l\} $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{$r$:rng\{i:l\}$\mid$ comm(rng\_car($r$); rng\_times($r$))\}